package com.graphcoloring;

import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ISolver;

import java.util.List;

public class NaiveEncodingSolverMoreClauses implements Solver {
    public Solution solve(GraphInputData data) throws Exception {
        int n = data.getVertexNumber();
        List<Integer[]> edges = data.getEdgeList();

        int colorCount = n;
        int colors[] = new int[n];
        for (int k = n; k >= 1; k--) {
        	
            ISolver solver = SolverFactory.newDefault();
            solver.setTimeout(60);
            solver.newVar(n * k + 1);

            for (Integer[] edge : edges) {
                int vertex1 = edge[0] + 1;
                int vertex2 = edge[1] + 1;

                for (int j = 0; j < k; j++) {
                    int clause[] = {-(vertex1 * k - j), -(vertex2 * k - j)};
                    solver.addClause(new VecInt(clause));
                }
            }
            for (int i = 1; i <= n; i++) {
                int clause[] = new int[k];
                for (int j = 0; j < k; j++) {
                    clause[j] = i * k - j;
                }
                solver.addClause(new VecInt(clause));
            }
            
            // new Clauses V1 -> -V2,-V3,...,-Vk and  V2 -> -V1,-V3,...,-Vk and  V3 -> -V2,-V1,...,-Vk and ... and  Vk -> -V2,-V3,...,-V1
            for (int i = 1; i <= n; i++) {
                for (int j1 = 0; j1 < k; j1++) {
                	for (int j2 = 0; j2 < k && j1!=j2; j2++) {
                		int clause[] = {-(i * k - j1), -(i * k - j2)};
                		solver.addClause(new VecInt(clause));
                    }
                }
                
            }
            
            if (solver.isSatisfiable()) {
                colorCount = k;

                int[] model = solver.model();
                for (int var : model) {
                    if (var > 0) {
                        int vertex = (var - 1) / k;
                        int color = (var - 1 + k) % k;
                        colors[vertex] = color;
                    }
                }
            } else {
                Solution solution = new Solution();
                solution.colorCount = colorCount;
                solution.colors = colors;

                return solution;


            }

        }
        return null;
    }
}
